package Syntaxe;

import java.util.LinkedHashSet;
import java.util.LinkedList;

import Simplification.PreSimplification;
import Simplification.Simplification;

public class Verification {

	public LinkedHashSet<String> SetVar;
	public int numVar;

	public Verification(LinkedHashSet<String> set) {
		SetVar = set;
		numVar = set.size();
	}

	public VecExpr inVector(Expression expr) {
		Fraction[] f = new Fraction[numVar];
		int i = 0;
		for (String s : SetVar) {
			f[i] = expr.subList.get(s);
			i++;
		}
		return new VecExpr(f, expr.constantOfExpression);
	}

	public Fraction minExpr(Expression expr, Invariant inv) {
		// to check if expr>=0 dans Inv
		VecExpr vec = inVector(expr);
		PreSimplification pre = new PreSimplification(inv, SetVar);

		// debug
		pre.standard().AfficheMatrice();

		Fraction min = Simplification.minimise(pre.standard(),
				pre.foncExtend(vec.sublist));

		return min.plus(vec.constant);
	}

	public boolean isIncludedIn(Invariant inv1, Invariant inv2) {
		// to check if inv1 dans inv2
		LinkedList<Expression> list = new LinkedList<Expression>();
		list = inv2.listExpr;

		while (!list.isEmpty()) {
			Expression expr = list.poll();
			VecExpr vec = inVector(expr);
			PreSimplification pre = new PreSimplification(inv1,SetVar);

			// debug
			pre.standard().AfficheMatrice();

			Fraction min = Simplification.minimise(pre.standard(),
					pre.foncExtend(vec.sublist));
			min = min.plus(vec.constant);// plus constant de expression
			if (min.strictNegative()) {
				return false;
			}
		}
		return true;
	}
	public void simpInv(Invariant inv){
		LinkedList<Expression> list=new LinkedList<Expression>();
		list=inv.listExpr;//TODO 
		while(list.isEmpty()){
			Expression expr=list.poll();
			this.minExpr(list.poll(), inv)
		}
		
	}

}
